ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:ecl(ds; da), L,L':(event-info(ds;da) List), n,m:.
(ecl-halt(ds; da; x)(n,L))
 (ecl-halt(ds; da; x)(m,L'))
 compat(event-info(ds;da); L; L')
 guard(((L = L')  (n = m  ))) 

latex

Definitions

||as||, Y, reduce(f; k; as), concat(ll), if b then t else f fi , ff, tt, null(as), b, ge(i; j), compat(T; l1; l2), False, A, A  B, , sq_type(T), P  Q, A c B, spreadn(a; x,y,z.t(x;y;z)), True, T, P  Q, P  Q, subtype(S; T), top, event-info(ds;da), guard(T), x. t(x), t  T, prop{i:l}, P  Q, P  Q, x:A. B(x), l_exists(L; T; x.P(x)), star-append(T; P; Q), decidable(P), l_all(L; T; x.P(x)), iseg(T; l1; l2), append(as; bs), ma-valtype(da; k), x:A. B(x), x(s), ecl-halt(ds; da; x)

Lemmas

ecl-halt-nil, non neg length, length-append, iseg append, false wf, l all cons, ge wf, nat properties, l all wf2, length wf1, concat wf, iseg antisymmetry, compat symmetry, compat-iseg, decidable lt, iseg weakening, iseg transitivity, common iseg compat, le wf, iseg wf, iseg append0, subtype rel self, Knd sq, assert wf, not wf, cons member, l member wf, or functionality wrt iff, member append, append assoc, true wf, squash wf, compat-cons, compat-append2, append wf, append nil sq, Kind-deq wf, fpf-cap wf, compat-append, member wf, top wf, length wf nat, Id wf, Knd wf, fpf wf, eclcatch wf, eclthrow wf, eclact wf, eclrepeat wf, eclor wf, ecland wf, eclseq wf, bool wf, ma-valtype wf, decl-state wf, eclbase wf, ecl wf, guard wf, compat wf, ecl-halt wf, nat wf, event-info wf, ecl-induction